T:Type, L:T List, n:, f:(n||L||).
increasing(f;n)  (L1:T List. ||L1|| = n   & sublist_occurence(T;L1;L;f)) 

latex

Definitions	t  T, x:A. B(x), ||as||, {i..j}, , S  T, S  T, increasing(f;k), P & Q, A & B, x:A. B(x), P  Q, False, A, AB, sublist_occurence(T;L1;L2;f), i  j < k, P  Q, Dec(P), {T}, SQType(T), l[i], Prop, ij, hd(l), i<j, ij, P  Q, P  Q, fadd(f;g), nondecreasing(f;k), True, T
Lemmas	squash wf, fadd increasing, const nondecreasing, select cons tl, increasing lower bound, length cons, non neg length, select wf, nat sq, decidable int equal, le wf, length wf2, nat wf, increasing wf, int seg wf, length wf1